COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	apply.ax[e81,jmc]	EKL axioms for apply and eval for making recursive function defs
C00007 ENDMK
C⊗;
apply.ax[e81,jmc]	EKL axioms for apply and eval for making recursive function defs

1. We shalll define recursive functions by EKL statements of the form

(DEFINE |append = λu v.apply(APP,<u,v>,appdef)|)

together with

(DEFINE |appdef = (<APP LAMBDA (U V) (IF (NULL U) V (CONS (CAR U) (APP (CDR U) V)))))|).

These are definitions rather than axioms, so they do not allow the user of EKL
to sneak in assumptions as part of his purported function definitions.  In fact
we suppose a version of EKL that doesn't allow users to give axioms.  Thus EKL
certifies anything proved about the defined functions.

2. We will use the above definitions together with the axiomatization of eval
and apply to prove the equation

∀u v.append(u,v) = if null u then v else car u . append(cdr u,v)

which we have heretofore written as an axiom.

3. Proving that  append  as defined above satisfies the recursion equation
seems to go better with definitions of  apply  and  eval  than have been used
previously, but some of the changes may have other virtues.  Some of the
features of these definitions may have been included in other people's
evals.

	The functions use an a-list, but instead of  consing new pairs on
the front of the a-list, we make a new a-list which has only one occurrence
of the variable.  The new function can be called  assign  and can be defined

assign(var,val,a-list) ← if null a-list then <[var.val]>
	else if var = caar a-list then [var.val] . cdr a-list
	else car a-list . assign(var,val,cdr a-list).

This version puts a new variable at the end of the a-list, but a version
that puts it on the front can also be given.  From our present point of
view, the advantage of  assign  is that we will finish with the same a-list
with which we start, and this will facilitate proving the recursion
equation.  The practical advantage might be that the length of the
a-list won't grow with recursion depth, so that the time
required to look up a variable will depend on the number of variables
and not on recursion depth.  The mathematics of  assign  will be the
same as as that of the  a  function of (McCarthy and Painter).

4. We have

eval(e,a) ← if atom e then cdr assoc(e,a)
	else if car e = IF then
		[if evalp(cadr e,a) then eval(caddr e,a) else eval(cadddr e,a)]
	else apply(car e,evlis(cdr e,a),a)

apply(fn,args,a) = if fn = CAR then car car args
	else if fn = CDR then cdr car args
	else if fn = CONS then car args . cadr args
	else if atom fn then apply(cdr assoc(fn,a),args,a)
	else if caar fn = LAMBDA then
		eval(caddr fn,prup(cadr fn,args,a))

prup(vars,args,a) ← if null vars then a
	else assign(car vars,car args,prup(cdr vars,cdr args,a))

evalp(p,a) ←

[To be given later, but it is important to note that  evalp  does not provide
for recursive predicates, which avoids (we hope) an opportunity for
inconsistency].